0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 81 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 21 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 2 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
maxC_in_aga(s(T13), 0, s(T13)) → maxC_out_aga(s(T13), 0, s(T13))
maxC_in_aga(s(T24), s(T22), s(T24)) → U3_aga(T24, T22, lessA_in_ga(T22, T24))
lessA_in_ga(0, s(T31)) → lessA_out_ga(0, s(T31))
lessA_in_ga(s(T36), s(T38)) → U1_ga(T36, T38, lessA_in_ga(T36, T38))
U1_ga(T36, T38, lessA_out_ga(T36, T38)) → lessA_out_ga(s(T36), s(T38))
U3_aga(T24, T22, lessA_out_ga(T22, T24)) → maxC_out_aga(s(T24), s(T22), s(T24))
maxC_in_aga(0, T54, T54) → maxC_out_aga(0, T54, T54)
maxC_in_aga(s(T61), T60, T60) → U4_aga(T61, T60, lessB_in_ag(T61, T60))
lessB_in_ag(0, s(T68)) → lessB_out_ag(0, s(T68))
lessB_in_ag(s(T75), s(T74)) → U2_ag(T75, T74, lessB_in_ag(T75, T74))
U2_ag(T75, T74, lessB_out_ag(T75, T74)) → lessB_out_ag(s(T75), s(T74))
U4_aga(T61, T60, lessB_out_ag(T61, T60)) → maxC_out_aga(s(T61), T60, T60)
maxC_in_aga(s(T94), T93, T93) → U5_aga(T94, T93, lessB_in_ag(T94, T93))
U5_aga(T94, T93, lessB_out_ag(T94, T93)) → maxC_out_aga(s(T94), T93, T93)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
maxC_in_aga(s(T13), 0, s(T13)) → maxC_out_aga(s(T13), 0, s(T13))
maxC_in_aga(s(T24), s(T22), s(T24)) → U3_aga(T24, T22, lessA_in_ga(T22, T24))
lessA_in_ga(0, s(T31)) → lessA_out_ga(0, s(T31))
lessA_in_ga(s(T36), s(T38)) → U1_ga(T36, T38, lessA_in_ga(T36, T38))
U1_ga(T36, T38, lessA_out_ga(T36, T38)) → lessA_out_ga(s(T36), s(T38))
U3_aga(T24, T22, lessA_out_ga(T22, T24)) → maxC_out_aga(s(T24), s(T22), s(T24))
maxC_in_aga(0, T54, T54) → maxC_out_aga(0, T54, T54)
maxC_in_aga(s(T61), T60, T60) → U4_aga(T61, T60, lessB_in_ag(T61, T60))
lessB_in_ag(0, s(T68)) → lessB_out_ag(0, s(T68))
lessB_in_ag(s(T75), s(T74)) → U2_ag(T75, T74, lessB_in_ag(T75, T74))
U2_ag(T75, T74, lessB_out_ag(T75, T74)) → lessB_out_ag(s(T75), s(T74))
U4_aga(T61, T60, lessB_out_ag(T61, T60)) → maxC_out_aga(s(T61), T60, T60)
maxC_in_aga(s(T94), T93, T93) → U5_aga(T94, T93, lessB_in_ag(T94, T93))
U5_aga(T94, T93, lessB_out_ag(T94, T93)) → maxC_out_aga(s(T94), T93, T93)
MAXC_IN_AGA(s(T24), s(T22), s(T24)) → U3_AGA(T24, T22, lessA_in_ga(T22, T24))
MAXC_IN_AGA(s(T24), s(T22), s(T24)) → LESSA_IN_GA(T22, T24)
LESSA_IN_GA(s(T36), s(T38)) → U1_GA(T36, T38, lessA_in_ga(T36, T38))
LESSA_IN_GA(s(T36), s(T38)) → LESSA_IN_GA(T36, T38)
MAXC_IN_AGA(s(T61), T60, T60) → U4_AGA(T61, T60, lessB_in_ag(T61, T60))
MAXC_IN_AGA(s(T61), T60, T60) → LESSB_IN_AG(T61, T60)
LESSB_IN_AG(s(T75), s(T74)) → U2_AG(T75, T74, lessB_in_ag(T75, T74))
LESSB_IN_AG(s(T75), s(T74)) → LESSB_IN_AG(T75, T74)
MAXC_IN_AGA(s(T94), T93, T93) → U5_AGA(T94, T93, lessB_in_ag(T94, T93))
maxC_in_aga(s(T13), 0, s(T13)) → maxC_out_aga(s(T13), 0, s(T13))
maxC_in_aga(s(T24), s(T22), s(T24)) → U3_aga(T24, T22, lessA_in_ga(T22, T24))
lessA_in_ga(0, s(T31)) → lessA_out_ga(0, s(T31))
lessA_in_ga(s(T36), s(T38)) → U1_ga(T36, T38, lessA_in_ga(T36, T38))
U1_ga(T36, T38, lessA_out_ga(T36, T38)) → lessA_out_ga(s(T36), s(T38))
U3_aga(T24, T22, lessA_out_ga(T22, T24)) → maxC_out_aga(s(T24), s(T22), s(T24))
maxC_in_aga(0, T54, T54) → maxC_out_aga(0, T54, T54)
maxC_in_aga(s(T61), T60, T60) → U4_aga(T61, T60, lessB_in_ag(T61, T60))
lessB_in_ag(0, s(T68)) → lessB_out_ag(0, s(T68))
lessB_in_ag(s(T75), s(T74)) → U2_ag(T75, T74, lessB_in_ag(T75, T74))
U2_ag(T75, T74, lessB_out_ag(T75, T74)) → lessB_out_ag(s(T75), s(T74))
U4_aga(T61, T60, lessB_out_ag(T61, T60)) → maxC_out_aga(s(T61), T60, T60)
maxC_in_aga(s(T94), T93, T93) → U5_aga(T94, T93, lessB_in_ag(T94, T93))
U5_aga(T94, T93, lessB_out_ag(T94, T93)) → maxC_out_aga(s(T94), T93, T93)
MAXC_IN_AGA(s(T24), s(T22), s(T24)) → U3_AGA(T24, T22, lessA_in_ga(T22, T24))
MAXC_IN_AGA(s(T24), s(T22), s(T24)) → LESSA_IN_GA(T22, T24)
LESSA_IN_GA(s(T36), s(T38)) → U1_GA(T36, T38, lessA_in_ga(T36, T38))
LESSA_IN_GA(s(T36), s(T38)) → LESSA_IN_GA(T36, T38)
MAXC_IN_AGA(s(T61), T60, T60) → U4_AGA(T61, T60, lessB_in_ag(T61, T60))
MAXC_IN_AGA(s(T61), T60, T60) → LESSB_IN_AG(T61, T60)
LESSB_IN_AG(s(T75), s(T74)) → U2_AG(T75, T74, lessB_in_ag(T75, T74))
LESSB_IN_AG(s(T75), s(T74)) → LESSB_IN_AG(T75, T74)
MAXC_IN_AGA(s(T94), T93, T93) → U5_AGA(T94, T93, lessB_in_ag(T94, T93))
maxC_in_aga(s(T13), 0, s(T13)) → maxC_out_aga(s(T13), 0, s(T13))
maxC_in_aga(s(T24), s(T22), s(T24)) → U3_aga(T24, T22, lessA_in_ga(T22, T24))
lessA_in_ga(0, s(T31)) → lessA_out_ga(0, s(T31))
lessA_in_ga(s(T36), s(T38)) → U1_ga(T36, T38, lessA_in_ga(T36, T38))
U1_ga(T36, T38, lessA_out_ga(T36, T38)) → lessA_out_ga(s(T36), s(T38))
U3_aga(T24, T22, lessA_out_ga(T22, T24)) → maxC_out_aga(s(T24), s(T22), s(T24))
maxC_in_aga(0, T54, T54) → maxC_out_aga(0, T54, T54)
maxC_in_aga(s(T61), T60, T60) → U4_aga(T61, T60, lessB_in_ag(T61, T60))
lessB_in_ag(0, s(T68)) → lessB_out_ag(0, s(T68))
lessB_in_ag(s(T75), s(T74)) → U2_ag(T75, T74, lessB_in_ag(T75, T74))
U2_ag(T75, T74, lessB_out_ag(T75, T74)) → lessB_out_ag(s(T75), s(T74))
U4_aga(T61, T60, lessB_out_ag(T61, T60)) → maxC_out_aga(s(T61), T60, T60)
maxC_in_aga(s(T94), T93, T93) → U5_aga(T94, T93, lessB_in_ag(T94, T93))
U5_aga(T94, T93, lessB_out_ag(T94, T93)) → maxC_out_aga(s(T94), T93, T93)
LESSB_IN_AG(s(T75), s(T74)) → LESSB_IN_AG(T75, T74)
maxC_in_aga(s(T13), 0, s(T13)) → maxC_out_aga(s(T13), 0, s(T13))
maxC_in_aga(s(T24), s(T22), s(T24)) → U3_aga(T24, T22, lessA_in_ga(T22, T24))
lessA_in_ga(0, s(T31)) → lessA_out_ga(0, s(T31))
lessA_in_ga(s(T36), s(T38)) → U1_ga(T36, T38, lessA_in_ga(T36, T38))
U1_ga(T36, T38, lessA_out_ga(T36, T38)) → lessA_out_ga(s(T36), s(T38))
U3_aga(T24, T22, lessA_out_ga(T22, T24)) → maxC_out_aga(s(T24), s(T22), s(T24))
maxC_in_aga(0, T54, T54) → maxC_out_aga(0, T54, T54)
maxC_in_aga(s(T61), T60, T60) → U4_aga(T61, T60, lessB_in_ag(T61, T60))
lessB_in_ag(0, s(T68)) → lessB_out_ag(0, s(T68))
lessB_in_ag(s(T75), s(T74)) → U2_ag(T75, T74, lessB_in_ag(T75, T74))
U2_ag(T75, T74, lessB_out_ag(T75, T74)) → lessB_out_ag(s(T75), s(T74))
U4_aga(T61, T60, lessB_out_ag(T61, T60)) → maxC_out_aga(s(T61), T60, T60)
maxC_in_aga(s(T94), T93, T93) → U5_aga(T94, T93, lessB_in_ag(T94, T93))
U5_aga(T94, T93, lessB_out_ag(T94, T93)) → maxC_out_aga(s(T94), T93, T93)
LESSB_IN_AG(s(T75), s(T74)) → LESSB_IN_AG(T75, T74)
LESSB_IN_AG(s(T74)) → LESSB_IN_AG(T74)
From the DPs we obtained the following set of size-change graphs:
LESSA_IN_GA(s(T36), s(T38)) → LESSA_IN_GA(T36, T38)
maxC_in_aga(s(T13), 0, s(T13)) → maxC_out_aga(s(T13), 0, s(T13))
maxC_in_aga(s(T24), s(T22), s(T24)) → U3_aga(T24, T22, lessA_in_ga(T22, T24))
lessA_in_ga(0, s(T31)) → lessA_out_ga(0, s(T31))
lessA_in_ga(s(T36), s(T38)) → U1_ga(T36, T38, lessA_in_ga(T36, T38))
U1_ga(T36, T38, lessA_out_ga(T36, T38)) → lessA_out_ga(s(T36), s(T38))
U3_aga(T24, T22, lessA_out_ga(T22, T24)) → maxC_out_aga(s(T24), s(T22), s(T24))
maxC_in_aga(0, T54, T54) → maxC_out_aga(0, T54, T54)
maxC_in_aga(s(T61), T60, T60) → U4_aga(T61, T60, lessB_in_ag(T61, T60))
lessB_in_ag(0, s(T68)) → lessB_out_ag(0, s(T68))
lessB_in_ag(s(T75), s(T74)) → U2_ag(T75, T74, lessB_in_ag(T75, T74))
U2_ag(T75, T74, lessB_out_ag(T75, T74)) → lessB_out_ag(s(T75), s(T74))
U4_aga(T61, T60, lessB_out_ag(T61, T60)) → maxC_out_aga(s(T61), T60, T60)
maxC_in_aga(s(T94), T93, T93) → U5_aga(T94, T93, lessB_in_ag(T94, T93))
U5_aga(T94, T93, lessB_out_ag(T94, T93)) → maxC_out_aga(s(T94), T93, T93)
LESSA_IN_GA(s(T36), s(T38)) → LESSA_IN_GA(T36, T38)
LESSA_IN_GA(s(T36)) → LESSA_IN_GA(T36)
From the DPs we obtained the following set of size-change graphs: